Skip to content

fix(ci): make the secret scanner and the Lean proof gate actually run - #129

Merged
hyperpolymath merged 1 commit into
mainfrom
fix/valid-workflows-secret-scanner-and-lean-proofs
Jul 27, 2026
Merged

fix(ci): make the secret scanner and the Lean proof gate actually run#129
hyperpolymath merged 1 commit into
mainfrom
fix/valid-workflows-secret-scanner-and-lean-proofs

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Two workflows in this repo are rejected by Actions at parse time, before a runner is allocated. Neither has ever produced a result. Two independent faults, one per file.

1. secret-scanner.ymljobs: was empty

The job key scan: sat at column 0 — a sibling of jobs:, not a child:

jobs:
scan:            # <-- column 0
    permissions:
      ...

So jobs: parsed as null and Actions refused the file.

This is valid YAML but invalid Actions, which is why linting never caught it — a yaml.safe_load sweep over all 22 workflows here passes this file happily. Only Actions' own schema rejects it.

Consequence: the job-level permissions: block added in #124 is attached to a top-level key Actions ignores. That fix has been inert, and gitleaks has never executed in this repository. The diagnosis in #124 was right and the reusable SHA pin is correct and untouched — the fix simply never took effect.

Fix: indent scan: by two spaces. The child keys were already at 4, so the block nests correctly.

2. lean-proofs.yml — unquoted ": " in three step names

Parse error at line 60, column 63: mapping values are not allowed here. An unquoted YAML scalar cannot contain ": ", and three - name: values do:

(§7.1 not-regular: DFA + pigeonhole)
(§7.3 CFL closure: union/concat/star)
(§7.3 non-closure: pumping foundation)

Fix: quote all three.

This one inverts the usual failure mode. lean-proofs.yml is an honest gate — it installs the pinned Lean toolchain and runs lean <file> with no || true, and was written specifically to stop the bit-rot recorded in docs/proofs/verification/AUDIT.md. It is not a fake gate that passes when it shouldn't. It is a real gate that has never run.

The proofs behind it are green, verified locally before this PR:

prover result
6 × .lean Lean 4.30.0 (per lean-toolchain) all PASS
3 × .v Coq 8.20.1 all PASS

Trust base is clean: zero sorry, Admitted, axiom or Parameter. So nothing had rotted — the guard was simply switched off.

Verification

All 22 workflow files now pass a structural check mirroring what Actions requires: parses as a mapping, has a trigger, and jobs is a non-empty mapping in which every job has steps or uses.

Expect this PR itself to demonstrate the fix: lean-proofs triggers on changes to .github/workflows/lean-proofs.yml, so it should run here for the first time. Secret Scanner will also run for the first time — expect findings that need triage rather than a clean pass.

Recognising this class

Both faults share one signature, worth knowing:

  • the run is listed by file path instead of workflow name
  • gh run view --log-failed returns "log not found"
  • gh pr checks shows nothing at all — a parse-rejected workflow creates no check run

Only gh run list --json conclusion reveals them.

Estate note: the col-0 jobs: fault is not widespread. A scan of all 13,330 workflow files across hyper-repos/meta-repos/repos found it in exactly two — this repo and voyage-enterprise-decision-system, byte-identical in shape. That one is being fixed in the same pass.

🤖 Generated with Claude Code

Both workflows were rejected by Actions before a runner was ever
allocated, so neither gate has produced a single result in this repo.
Two independent parse faults, one per file.

secret-scanner.yml — the job key `scan:` sat at column 0, a sibling of
`jobs:` rather than a child, so `jobs:` parsed as null and Actions
refused the file. This is valid YAML but invalid Actions, which is why
YAML-based linting never flagged it: a `yaml.safe_load` sweep of all 22
workflows in this repo passes it. The practical consequence is that the
job-level `permissions:` block added in #124 was attached to a key
Actions ignores, so that fix has been inert and **gitleaks has never
executed here**. The reusable pin is untouched.

lean-proofs.yml — three `- name:` values contain an unquoted ": ", e.g.
"(§7.1 not-regular: DFA + pigeonhole)". An unquoted YAML scalar may not
contain ": ", so the file failed to parse at line 60. Quoted all three.

Worth stating plainly, because it inverts the usual failure mode in this
estate: lean-proofs.yml is an *honest* gate. It installs the pinned Lean
toolchain and runs `lean <file>` with no `|| true`. It is not a fake
gate that passes when it shouldn't — it is a real gate that has never
run. The proofs behind it are green (verified locally: 6 Lean under
pinned 4.30.0 and 3 Coq under 8.20.1 all pass, with zero sorry,
Admitted, axiom or Parameter), so nothing has rotted; the guard was
simply switched off.

Verification: all 22 workflow files now pass a structural check that
mirrors what Actions requires — parses as a mapping, has a trigger, and
`jobs` is a non-empty mapping whose every job has `steps` or `uses`.

Both faults produce the same signature and are worth recognising:
the run is listed by file path instead of workflow name, and
`gh run view --log-failed` returns "log not found". `gh pr checks`
shows nothing at all, because a parse-rejected workflow creates no
check run.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@hyperpolymath
hyperpolymath marked this pull request as ready for review July 27, 2026 18:08
@hyperpolymath
hyperpolymath merged commit 7864eb0 into main Jul 27, 2026
36 of 38 checks passed
@hyperpolymath
hyperpolymath deleted the fix/valid-workflows-secret-scanner-and-lean-proofs branch July 27, 2026 18:08
hyperpolymath added a commit to hyperpolymath/voyage-enterprise-decision-system that referenced this pull request Jul 27, 2026
…-sync (#53)

Two workflows in this repository are rejected by Actions **at parse
time**, so neither has ever produced a result.

## 1. `secret-scanner.yml` — `jobs:` was empty

The job key `scan:` sat at **column 0**, a sibling of `jobs:` rather
than a child, so `jobs:` parsed as `null` and Actions refused the file.
**Every `Secret Scanner` run in this repository has ended in
`startup_failure`, meaning gitleaks has never executed here.**

This is **valid YAML but invalid Actions**, so YAML-based linting
doesn't catch it — a `yaml.safe_load` sweep over this repo's workflows
passes the file happily. Only Actions' own schema rejects it.

The knock-on: the job-level `permissions:` block granting the
`pull-requests: write` and `actions: read` that the reusable's gitleaks
job requires was attached to a top-level key Actions ignores, so it
never took effect. The reusable SHA pin is untouched.

Fix: indent `scan:` by two spaces. Its child keys were already at four.

## 2. `instant-sync.yml` — misplaced step broke the parse

A sweep appended a `K9-SVC Validation` step at **two-space** indentation
— job-key level — instead of the six spaces that would put it inside the
`dispatch` job's `steps:` list. YAML hit a sequence item where it
expected a block mapping and failed at line 36.

Consequence: **Instant Sync has been `startup_failure` here, so forge
propagation has not been running.**

Re-indented the step and its body. The job now parses with its three
steps as intended.

## Recognising this class

Both faults share a signature:

- the run is listed by **file path** instead of workflow name
- `gh run view --log-failed` returns **"log not found"**
- `gh pr checks` shows **nothing** — a parse-rejected workflow creates
no check run

Only `gh run list --json conclusion` reveals them.

## Estate context

- The col-0 `jobs:` fault is **narrow**: a scan of all 13,330 workflow
files across `hyper-repos`/`meta-repos`/`repos` found it in exactly
**two** repositories — this one and `wokelang`, byte-identical in shape.
wokelang is fixed in hyperpolymath/wokelang#129.
- The misplaced `K9-SVC Validation` step is **not** narrow — the same
mis-indentation appears in **59 workflow files** estate-wide (against 12
correctly indented). Reported separately.

## Note on branching

Branched from `origin/main` deliberately. The local checkout carried two
unpushed sweep-authored commits (`chore: estate-wide security
compliance`, `chore: remove duplicate GOVERNANCE files`) that are not
part of this fix and were not inherited.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request Jul 27, 2026
…tly (#130)

Follow-on to #129. That PR made the two dead gates *run*; this one makes
the remaining four checks *pass*, and replaces four config files that a
sweep had overwritten with generic estate boilerplate.

## Gates

### Rust CI — `clippy -D warnings` (was exit 101)

~32 lints. Most came straight from `cargo clippy --fix`. Two groups
needed judgement:

- **19 × `&[x.clone()]` → `std::slice::from_ref(&x)`** — single-element
slices; drops a needless clone.
- **5 × `clippy::approx_constant` — a false positive.** Every hit is the
literal `3.14` used as arbitrary decimal test data: `abs(-3.14) ==
3.14`, a JSON float round-trip, a channel send/receive. None of them
mean π. Substituting `std::f64::consts::PI` would change what the tests
assert, so the test modules carry a narrowly scoped `#[allow]` with the
reason written beside it.

**This failure was masking three other jobs.** `Cargo audit`, `Cargo
test` and `Coverage` were all `skipped` behind it. Tests now actually
run: **236 pass, 0 fail.**

### Cargo Audit + Security — RUSTSEC-2026-0190

Both were red on the same advisory (unsoundness in `anyhow`'s
`Error::downcast_mut()`).

The plan was a time-boxed `audit.toml` ignore. It turned out not to be
needed: `anyhow` is transitive and **1.0.104 is released**, so this is a
real fix. Bumped `1.0.102 → 1.0.104`; `cargo audit -D warnings` now
exits 0. **No suppression file added.**

### ClusterFuzzLite — `open Dockerfile: no such file or directory`

`.clusterfuzzlite/` holds a `Containerfile` per the estate's
podman-first naming, but ClusterFuzzLite hardcodes
`.clusterfuzzlite/Dockerfile`. Added `Dockerfile` as a **symlink** to
`Containerfile` (git mode `120000`), so the tool finds the name it
demands while the estate convention remains the single source of truth.

## Config files

These carried generic multi-language boilerplate that didn't describe
this repo — and in two cases actively contradicted it.

| File | What was wrong |
|---|---|
| `mise.toml` | `rust = "latest"` **against** `rust-toolchain.toml`'s
deliberate `1.96.0` pin; declared
node/python/go/java/bun/npm/yarn/pnpm/pip — **all BANNED by this repo's
own `.claude/CLAUDE.md`**; `[alias]` chained `cargo test \|\| npm test
\|\| go test ./...` |
| `.tool-versions` | `rust stable` — same contradiction |
| `.editorconfig` | Covered Elixir/ReScript/Zig/Ada; **omitted Lean,
Coq, ocamllex/menhir and `.woke`/`.wl`** |
| `.gitattributes` | Same — absent languages in, present languages out |
| `.gitignore` | Cruft for absent languages; missing `*.olean`,
`*.ilean`, `.lake/`, Idris `*.ttc` |
| `guix.scm` | Licence field that **could never have evaluated** |

Two of these deserve spelling out.

**The `mise.toml` alias block was a fake gate by construction.** `test =
"cargo test || npm test || go test ./..."` converts a genuine `cargo
test` failure into an attempt at two toolchains that don't exist here.
The pin contradiction matters for the same reason: `rust-toolchain.toml`
documents that a drifting `stable` once broke *this very clippy gate*
with lints local clippy couldn't see.

**`guix.scm`'s licence was broken two ways:**

```scheme
(license ((@@ (guix licenses) license) "MPL-2.0" "..."))
```

`@@` reaches into a **non-exported** binding, and the `license` record
constructor takes three fields but was given two. Because guix isn't
installed on the development host, nothing ever evaluated this file and
the fault sat unnoticed. Now `(license mpl2.0)` — what `(guix licenses)`
actually exports. Confirmed the file parses under guile and that the old
form raises `unbound-variable`.

`.gitignore` was checked both directions: no currently tracked file
becomes ignored, and the tracked `examples/math.wasm` fixture is
explicitly re-included.

## Verified locally

```
cargo clippy --workspace --all-targets -- -D warnings   PASS
cargo fmt --all -- --check                              PASS
cargo test --workspace                                  PASS (236 tests)
cargo audit -D warnings                                 PASS
guix.scm parses under guile                             PASS
all 22 workflows structurally valid for Actions         PASS
no tracked file newly ignored                           PASS
```

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant